This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
By now you should be getting suspicious that all is not quite right. We will
now justify your discomfort. First, our proposed description of the meaning
of λ-notation is a bit too cavalier. Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
and %2not%* when the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#[%aS%9*%1#→#%aS%*] rather than
simply %aS%9*%1#→#%aS%1. Is this consistent with our understanding of the
meaning of λ-notation? Yes. 
It is exactly what %2⊗→closure↔←%* was attempting to 
describe. What we previously have called an ⊗→open function↔← is a creature of the
form: 
 %aS%9*%1#→#%aS%*.

.END
 This enlightened view of λ-notation must change our conception on %denv%* as well.
Now, given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. I.e. for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END
We will let you ponder the significance of this statement for a few moments
while we continue the discussion of "<=".

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=#%9D%4a%1{%ag%1}%d(l#:#<f,%9D%4a%1{%ag%1}%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; T → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation as input and will return as value a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it requires the minimal structure on the function.
⊗↓Like a free group satisfies the group axioms, but imposes no other
requirements.← 
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. Though a full discussion of "least" brings in the recent work of D. Scott
and is a bit too advanced for our purposes, the intuition behind
this study is quite accessible and again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).
Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; T → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%aU%*>,<1,%aU%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%aU%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's.
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\| n%82%1 if %d0%c≤%dn%c≤%di
f%4i%*\<
\| %aU%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.

In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %aU%*#⊗↓We 
perhaps should subscript %aU%* to distinguish it from previous %aU%*'s.←.


.BEGIN CENTER;
%9t%d(%aU%*) = %9λ%d((n) cond(n=0, 0, %aU%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%aU%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%aU%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %aU%1.← we can say
.BEGIN CENTER;GROUP;

%df%4n%* = %9t%8n%d(%aU%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%aU%d)%1.
.END

Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4n→∞%9t%8n%d(%aU%d).%1
.END
Thus in summary, %dY%* is a mapping:[%aFn%* → %aFn%*] → %aFn%*
such that if %9t%*#%9ε%*#[%aFn%*#→#%aFn%*] and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END

So the search for denotations for %3label%* might be better served by:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%1{%ag%*}%d(l%1#:#%d<f,h>))%1.
.END


Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %3f=g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?
.BEGIN TURN OFF "{","}";TURN ON "#";
First, the characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%1{%3label[car;car][(A#B)]%1} will exhibit a discrepancy.
.END

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.

***add lisp induction***


The intuitions presented in this section can be made very  precise. 
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.

*** ADD MONOTONICITY, CONTINUITY

The papers of Scott, Gordon, and Wadsworth supply the missing precision.
In case you think least fixed points are too removed from the realities of
programming language design, please refer to {yon(P94)} again.
Though intuition finally uncovered a counterexample to the general application
of the specific implementation of LISP's %3label%*, intuition has been guilty
of superficiality here. The nature of recursion is a difficult question and
this fixpoint approach should make us aware of the pitfalls.


Actually we glossed over a different kind of fixed point a few moments
ago:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1]
.END

This statement requires a fixed point interpretation to be meaningful.
Finally stirring denotations for simple variables back into our %denv%*,
we are led to an adequate description of environments for LISP:

.BEGIN CENTERIT;
←%denv%1 is the set of functions  %aId%1 → [%denv%1 → %aFn%1∪%aS%1]
.END

**structure of domains**

**justification**

Recalling that  this characterization of %denv%* arose in explicating
free variables, it should  not come as too much of a suprise that
we must modify the fix-point characterization of %3label[f;g]%*.
We had assumed that %3f%* and %3g%* were in %aFn%*, whereas they are
in %denv%*→%aFn%1. %3label[f;g]%* binds %3f%* to %3g%* in an environment,
leaving free variables in %3g%* unassigned. These free variables of %3g%*
are evaluated in the environment current when the %3label%*-expression
is applied. Thus the meaning of a %3label%*-expression should also be a
member of %denv%*→%aFn%1. So:

.BEGIN TURN OFF "{","}";CENTERIT;FILL;TURN ON "#";
←%9D%4a%1{%3label[%af%1;%ag%*]}%d(l)%1#=
#%dY(%9λ%d(h)(%9λ%d(l%9*%d)(%9D%4a%1{%ag%*}%d(l%9*%1#:#%d<f,h>)) ))(l)%1.
.END

Notice that all our work on fixed-points  and recursion equations has only
involved %2single%* equations. Indeed, the label operator can only define
a single function. Frequently a function needs to be defined via a %2set%*
of recursion equations. In particular when we wrote %3eval%* and %3apply%*
we were really asking  for the solution  to such a set of equations: %2⊗→mutual recursion↔← equations%*.
When we wrote:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\eval <= λ[[e;a] ... 
\apply <= λ[[fn;x;a] ...
.END

As we said in {yonss(P38)}, we really meant:

.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; λ[[e;a] ... ]
\label[apply; λ[[fn;x;a] ...]
%1 where %3eval%* and %3apply%* occur within the %3λ%*-expressions.
.END

That is:
.BEGIN TABIT1(30);SELECT 3;GROUP;
\label[eval; %9F%1(%3eval,apply%1)]
\%3label[apply; %9Q%1(%3eval,apply%1)]
.END

Now since LISP doesn't allow %3label%* to express mutual recursion directly,
we must resort to a subterfuge if we wish to express such constructions in LISP.

Namely:
.BEGIN CENTER;SELECT 3;

label[eval; %9F%1(%3eval,label[apply; %9Q%1(%3eval,apply%1)]%1)]

.END

Clearly this subterfuge is applicable to the definition of other
(mutually recursive) functions; but subterfuge, it is. To really be
useful, we realize that LISP must at least allow a %2sequence%* of
definitions to be given such that these definitions will be in effect
through some  reasonable calculation. 
There is minimal insight gained by thinking
of our LISP functions as anonymous solutions to a gigantic fixpoint equation.
Sequencing, thus is important. Sequencing is implicit in the order
of evaluation of arguments expressed in %3eval%*; sequencing is 
implicit in the evaluation of ⊗→special form↔←s. 
Certainly sequencing has become quite explicit by the time we examine %3prog%*.
All of these  manifestations of sequencing have been abstracted out in the
denotational approach. 
It is natural to ask whether there is  some way to introduce
sequencing into our formalism so that more realistic implementations
can be proved correct.

***continuations: extensions to sequencing and order of evaluation***

After all this work there really should be a comparable return on
on our investment. We believe there is. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages. 
A clearer perception of the role of definition and computation.
Later we will see that the thought required to specify domains and 
ranges of functions is directly applicable to 
the design of an extension to LISP which allows user-defined
data structures.



.CENT(Problems);
%2I%*  What is the %2statement%* of the correctness of %3eval%* in terms
of the denotational semantics?